import java.awt.Dimension;
import java.awt.EventQueue;

import javax.swing.JFrame;
import javax.swing.JTree;
import java.awt.BorderLayout;
import javax.swing.tree.DefaultTreeModel;
import javax.swing.tree.DefaultMutableTreeNode;
import javax.swing.tree.TreeModel;
import javax.swing.tree.TreeNode;
import javax.swing.tree.TreePath;
import javax.swing.JList;
import javax.swing.AbstractListModel;
import javax.swing.JPanel;
import java.awt.FlowLayout;
import java.awt.GridBagLayout;
import java.awt.GridBagConstraints;
import java.awt.Insets;
import java.awt.ComponentOrientation;

import org.apache.commons.lang3.StringUtils;
import org.apache.log4j.BasicConfigurator;
import org.apache.log4j.Logger;

import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;

import att.grappa.Graph;
import att.grappa.GrappaAdapter;
import att.grappa.GrappaPanel;
import att.grappa.GrappaSupport;
import att.grappa.Parser;

import pl.edu.pw.elka.dzielins.revanalyzer.GraphUtil;
import pl.edu.pw.elka.dzielins.revanalyzer.Project;
import pl.edu.pw.elka.dzielins.revanalyzer.Revanalyzer;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.AlloyException;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.io.Reader;
import pl.edu.pw.elka.dzielins.revanalyzer.alloy.io.Writer;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.InstanceObject;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.InstanceRelation;
import pl.edu.pw.elka.dzielins.revanalyzer.model.Model;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelFact;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelObject;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelRelation;

import java.awt.Component;
import javax.swing.BoxLayout;
import javax.swing.border.BevelBorder;
import javax.swing.DefaultCellEditor;
import javax.swing.JComboBox;
import javax.swing.JFileChooser;
import javax.swing.JMenuBar;
import javax.swing.JOptionPane;
import javax.swing.JPopupMenu;
import javax.swing.JSplitPane;
import javax.swing.JMenu;
import javax.swing.JMenuItem;
import javax.swing.ListSelectionModel;

import java.awt.event.MouseAdapter;
import java.awt.event.MouseEvent;
import javax.swing.Box;
import javax.swing.JScrollPane;
import java.awt.Rectangle;
import java.io.ByteArrayInputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStream;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;

import javax.swing.event.TableModelEvent;
import javax.swing.event.TableModelListener;
import javax.swing.event.TreeSelectionListener;
import javax.swing.event.TreeSelectionEvent;
import javax.swing.ScrollPaneConstants;
import javax.swing.JTable;
import javax.swing.table.DefaultTableModel;
import java.awt.event.KeyAdapter;
import java.awt.event.KeyEvent;
import javax.swing.JButton;
import java.awt.event.ActionListener;
import java.awt.event.ActionEvent;


public class MainWindow {
	
	private static final Logger LOG = Logger.getLogger(MainWindow.class);

	private JFrame frame;
	private JTree tree;
	private JScrollPane jsp;
	
	private Project project;
	private JTable table;

	/**
	 * Launch the application.
	 */
	public static void main(String[] args) {
		EventQueue.invokeLater(new Runnable() {
			public void run() {
				try {
					MainWindow window = new MainWindow();
					window.frame.setVisible(true);
				} catch (Exception e) {
					e.printStackTrace();
				}
			}
		});
	}

	/**
	 * Create the application.
	 */
	public MainWindow() {
		BasicConfigurator.configure();
		initialize();
	}

	/**
	 * Initialize the contents of the frame.
	 */
	private void initialize() {
		frame = new JFrame();
		frame.setResizable(false);
		frame.setBounds(100, 100, 600, 450);
		frame.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
		
		JMenuBar menuBar = new JMenuBar();
		frame.setJMenuBar(menuBar);
		
		JMenu mnNewMenu = new JMenu("File");
		menuBar.add(mnNewMenu);
		
		JMenuItem mntmOpenModel = new JMenuItem("Open model");
		mntmOpenModel.addMouseListener(new MouseAdapter() {
			@Override
			public void mousePressed(MouseEvent e) {
				LOG.debug("Showing JFileChooser to open module file");
				JFileChooser c = new JFileChooser();
				// Demonstrate "Open" dialog:
				int rVal = c.showOpenDialog(frame);
				if (rVal == JFileChooser.APPROVE_OPTION) {
					LOG.debug("Module file "+c.getSelectedFile().getAbsolutePath()+" chosen");
					loadModel(c.getSelectedFile());
				}
				if (rVal == JFileChooser.CANCEL_OPTION) {
					LOG.debug("No module file chosen");
				}
			}
		});
		mnNewMenu.add(mntmOpenModel);
		
		JMenuItem mntmWriteInstance = new JMenuItem("Write instance");
		mntmWriteInstance.addMouseListener(new MouseAdapter() {
			@Override
			public void mousePressed(MouseEvent arg0) {
				LOG.debug("Showing JFileChooser to save instance file");
				JFileChooser c = new JFileChooser();
				int rVal = c.showSaveDialog(frame);
				if (rVal == JFileChooser.APPROVE_OPTION) {
					LOG.debug("Module file "+c.getSelectedFile().getAbsolutePath()+" chosen");
					saveInstance(c.getSelectedFile());
				}
				if (rVal == JFileChooser.CANCEL_OPTION) {
					LOG.debug("No module file chosen");
				}
			}
		});
		mnNewMenu.add(mntmWriteInstance);
		frame.getContentPane().setLayout(new BorderLayout(0, 0));
		
		JPanel panel = new JPanel();
		frame.getContentPane().add(panel, BorderLayout.CENTER);
		GridBagLayout gbl_panel = new GridBagLayout();
		gbl_panel.columnWidths = new int[] {200, 400, 0};
		gbl_panel.rowHeights = new int[] {100, 0};
		gbl_panel.columnWeights = new double[]{1.0};
		gbl_panel.rowWeights = new double[]{0.0};
		panel.setLayout(gbl_panel);
		
		JPanel panel_3 = new JPanel();
		panel_3.setBorder(new BevelBorder(BevelBorder.LOWERED, null, null, null, null));
		GridBagConstraints gbc_panel_3 = new GridBagConstraints();
		gbc_panel_3.weighty = 1.0;
		gbc_panel_3.weightx = 1.0;
		gbc_panel_3.fill = GridBagConstraints.BOTH;
		gbc_panel_3.gridx = 1;
		gbc_panel_3.gridy = 0;
		panel.add(panel_3, gbc_panel_3);
		panel_3.setLayout(new BorderLayout(0, 0));
		
		jsp = new JScrollPane();
		jsp.getViewport().setBackingStoreEnabled(true);
	    
	    
	    
	    panel_3.add("Center", jsp);
	    
	    table = new JTable();
	    table.addKeyListener(new KeyAdapter() {
	    	@Override
	    	public void keyPressed(KeyEvent event) {
	    		if(event.getKeyCode() == 127 && table.getSelectedRow() != -1)
	    	    {
	    	        RevanalyzerTableModel model = (RevanalyzerTableModel) table.getModel();
	    	        model.removeRow(table.getSelectedRow());
	    	    }
	    	}
	    });
	    table.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
	    /*table.setModel(new DefaultTableModel(
	    	new Object[][] {
	    		{null, null, null},
	    		{null, null, null},
	    		{null, null, null},
	    	},
	    	new String[] {
	    		"New column", "New column", "New column"
	    	}
	    ));*/
	    jsp.setViewportView(table);
	    
	    JButton btnAddRecord = new JButton("Add record");
	    btnAddRecord.addActionListener(new ActionListener() {
	    	public void actionPerformed(ActionEvent arg0) {
	    	}
	    });
	    btnAddRecord.addMouseListener(new MouseAdapter() {
	    	@Override
	    	public void mouseClicked(MouseEvent event) {
	    		if (project != null)
	    			((RevanalyzerTableModel)table.getModel()).addNewRow();
	    	}
	    });
	    panel_3.add(btnAddRecord, BorderLayout.NORTH);
		
		JPanel panel_2 = new JPanel();
		panel_2.setBorder(new BevelBorder(BevelBorder.LOWERED, null, null, null, null));
		GridBagConstraints gbc_panel_2 = new GridBagConstraints();
		gbc_panel_2.weighty = 1.0;
		gbc_panel_2.weightx = 1.0;
		gbc_panel_2.fill = GridBagConstraints.BOTH;
		gbc_panel_2.gridx = 0;
		gbc_panel_2.gridy = 0;
		panel.add(panel_2, gbc_panel_2);
		GridBagLayout gbl_panel_2 = new GridBagLayout();
		gbl_panel_2.columnWidths = new int[]{200, 0};
		gbl_panel_2.rowHeights = new int[]{250, 200, 0};
		gbl_panel_2.columnWeights = new double[]{1.0, Double.MIN_VALUE};
		gbl_panel_2.rowWeights = new double[]{0.0, 1.0, Double.MIN_VALUE};
		panel_2.setLayout(gbl_panel_2);
		
		JScrollPane scrollPane = new JScrollPane();
		GridBagConstraints gbc_scrollPane = new GridBagConstraints();
		gbc_scrollPane.fill = GridBagConstraints.BOTH;
		gbc_scrollPane.insets = new Insets(0, 0, 5, 0);
		gbc_scrollPane.gridx = 0;
		gbc_scrollPane.gridy = 0;
		panel_2.add(scrollPane, gbc_scrollPane);
		
		tree = new JTree();
		tree.setModel(new DefaultTreeModel(
			new DefaultMutableTreeNode("JTree") {
				{
				}
			}
		));
		scrollPane.setViewportView(tree);
		tree.setToggleClickCount(0);
		tree.setRootVisible(false);
		
		tree.addMouseListener(new MouseAdapter() {
			/*private void myPopupEvent(MouseEvent e) {
				// show context menu
				int x = e.getX();
				int y = e.getY();
				JTree tree = (JTree) e.getSource();
				TreePath path = tree.getPathForLocation(x, y);
				if (path == null)
					return;

				tree.setSelectionPath(path);

				final Object obj = path.getLastPathComponent();
				final DefaultMutableTreeNode node = (DefaultMutableTreeNode) obj;
				String label = "popup: " + obj.toString();
				JPopupMenu popup = new JPopupMenu();
				JMenuItem item = new JMenuItem(label);
				item.addMouseListener(new MouseAdapter() {
					public void mousePressed(MouseEvent e) {
						LOG.info("Adding "+String.valueOf(obj));
						InstanceObject element = new InstanceObject(null, project.getModel().getObject(((ModelObject)(node.getUserObject())).getName()));
						project.getInstance().getObjects().add(element);
						refreshTree();
						refreshGraph();
					}
				});
				popup.add(item);
				popup.show(tree, x, y);
			}
			public void mousePressed(MouseEvent e) {
				if (e.isPopupTrigger())
					myPopupEvent(e);
			}
			public void mouseReleased(MouseEvent e) {
				if (e.isPopupTrigger())
					myPopupEvent(e);
			}*/
			@Override
			public void mouseClicked(MouseEvent event) {
				// get the object from clicked node
				int x = event.getX();
				int y = event.getY();
				JTree tree = (JTree) event.getSource();
				TreePath path = tree.getPathForLocation(x, y);
				if (path == null) {
					LOG.error("Cannot retrieve tree path");
					return;
				}
				Object clickedTreeNodeUserObject;				
				try {
					clickedTreeNodeUserObject = ((DefaultMutableTreeNode)path.getLastPathComponent()).getUserObject();
				} catch (Exception e) {
					LOG.error("Cannot retrieve clicked tree node object", e);
					return;
				}
				// handle clicks
				String[] columnNames;
				Object[][] data;
				if (clickedTreeNodeUserObject instanceof ModelObject) {
					LOG.info("Clicked tree object is ModelObject");
					table.setModel(new RevanalyzerTableModel(project, (ModelObject) clickedTreeNodeUserObject));
				} else if (clickedTreeNodeUserObject instanceof ModelRelation) {
					LOG.info("Clicked tree object is ModelRelation");
					table.setModel(new RevanalyzerTableModel(project, (ModelRelation) clickedTreeNodeUserObject));
					JComboBox columnCB;
					List<ModelObject> mArgs = ((ModelRelation) clickedTreeNodeUserObject).getArgumentsWithOwner();
					for (int i=0;i<mArgs.size();++i) {
						columnCB = new JComboBox();
						if (i != 0)
							columnCB.addItem(null);
						for(InstanceObject io : project.getInstanceObjectsFromModelObject(mArgs.get(i), true)) {
							columnCB.addItem(io);
						}
						table.getColumnModel().getColumn(i).setCellEditor(new DefaultCellEditor(columnCB));
					}
				} else {
					LOG.warn("Clicked tree object is neither ModelObject nor ModelRelation");
					return;
				}
				/*if (clickedTreeNodeUserObject instanceof ModelObject) {
					LOG.info("Clicked tree object is ModelObject");
					ModelObject mo = (ModelObject) clickedTreeNodeUserObject;
					// single column
					columnNames = new String[] { "Elements" };
					// data is instances
					List<InstanceObject> ios = project.getInstanceObjectsFromModelObject(mo);
					LOG.debug(String.valueOf(ios));
					data = new Object[ios.size()][1];
					for(int i = 0;i<ios.size();++i) {
						data[i] = new Object[] {ios.get(i)};
					}
					// set table model
					table.setModel(new DefaultTableModel(data, columnNames));
					// set table model listener
					table.getModel().addTableModelListener(new TableModelListener() {
						
						@Override
						public void tableChanged(TableModelEvent event) {
														
						}
						
					});
				} else if (clickedTreeNodeUserObject instanceof ModelRelation) {
					LOG.info("Clicked tree object is ModelRelation");
					ModelRelation mr = (ModelRelation) clickedTreeNodeUserObject;
					// get all relation arguments
					List<ModelObject> mArgs = mr.getArgumentsWithOwner();
					LOG.debug(String.valueOf(mArgs));
					// 0 element is relation owner
					// number of columns is number of relation's arguments
					columnNames = new String[mArgs.size()];
					// first column for owner
					columnNames[0] = "Argument 1 (Owner)";
					// next columns are generic
					for (int i=1;i<mArgs.size();++i) {
						columnNames[i] = "Argument " + String.valueOf(i+1);
					}
					// data is instances
					// get instances of owner object
					List<InstanceObject> ios = project.getInstanceObjectsFromModelObject(mr.getOwner());
					// get all relation instances
					List<InstanceRelation> irs = new LinkedList<InstanceRelation>();
					for (InstanceObject io : ios) {
						// TODO exceptions
						irs.addAll(io.getRelations().get(mr.getName()));
					}
					// set data
					data = new Object[irs.size()][mArgs.size()];
					for(int i = 0;i<irs.size();++i) {
						InstanceRelation ir = irs.get(i);
						Object[] record = new Object[mArgs.size()];
						List<InstanceObject> iArgs = ir.getArgumentsWithOwner();
						for (int j=0;j<iArgs.size();++j) {
							record[j] = iArgs.get(j);
						}
						data[i] = record;
					}
					// set table model
					table.setModel(new DefaultTableModel(data, columnNames));
					// set combo boxes as column editors
					JComboBox columnCB;
					for (int i=0;i<mArgs.size();++i) {
						columnCB = new JComboBox();
						for(InstanceObject io : project.getInstanceObjectsFromModelObject(mArgs.get(i))) {
							columnCB.addItem(io);
						}
						table.getColumnModel().getColumn(i).setCellEditor(new DefaultCellEditor(columnCB));
					}					
				} else {
					LOG.warn("Clicked tree object is neither ModelObject nor ModelRelation");
					return;
				}*/
			}
		});
		
		JScrollPane scrollPane_1 = new JScrollPane();
		GridBagConstraints gbc_scrollPane_1 = new GridBagConstraints();
		gbc_scrollPane_1.fill = GridBagConstraints.BOTH;
		gbc_scrollPane_1.gridx = 0;
		gbc_scrollPane_1.gridy = 1;
		panel_2.add(scrollPane_1, gbc_scrollPane_1);
		
		JPanel panel_1 = new JPanel();
		scrollPane_1.setViewportView(panel_1);
		
		JButton btnCheck = new JButton("Check");
		btnCheck.addMouseListener(new MouseAdapter() {
			@Override
			public void mouseClicked(MouseEvent arg0) {
				if (project == null)
					return;
				Revanalyzer revanalyzer = new Revanalyzer();
				try {
					A4Solution solution = revanalyzer.revanalyze(project.getModel(), project.getInstance());
					if (solution.satisfiable()) {
						LOG.info("Solution satisfiable");
						JOptionPane.showMessageDialog(frame,
							    "Instance valid");
						solution = solution.next();
						if (solution != null && solution.satisfiable()) {
							LOG.warn("Next instance found!");
						} else {
							LOG.info("Instance is valid!");
						}
					} else {
						LOG.info("Solution not satisfiable");
						Set<ModelFact> broken = null;
						if (project.getModel().getFacts().size()>1) {
							for (int i=project.getModel().getFacts().size()-1;i>0;i--) {
								boolean stop = false;
								Set<Model> models = project.getModel().getPartialModels(i);
								System.out.println(models.size());
								for (Model model : models) {
									System.out.println(model.getFacts().size());
									solution = revanalyzer.revanalyze(model, project.getInstance());
									if (solution.satisfiable()) {
										broken = project.getModel().getMissingFacts(model.getFacts());
										stop = true;
										break;
									}
								}
								if (stop)
									break;
							}
							
						} else {
							broken = project.getModel().getFacts();
						}	
						if (broken == null || broken.isEmpty()) {
							LOG.error("Cannot find solution and source of the error");
							JOptionPane.showMessageDialog(frame,
									"Cannot find solution and source of the error",
								    "Error",
								    JOptionPane.ERROR_MESSAGE);
						} else {
							LOG.info(String.valueOf(broken));
							String[] names = new String[broken.size()];
							int x=0;
							for (ModelFact fact :broken) {
								names[x] = fact.getName();
								x++;
							}
							if (names.length>1) {
								JOptionPane.showMessageDialog(frame,
									    StringUtils.join(names) + " are unsatisfied",
									    "Warning",
									    JOptionPane.WARNING_MESSAGE);
							}
							else {
								JOptionPane.showMessageDialog(frame,
									    StringUtils.join(names) + " is unsatisfied",
									    "Warning",
									    JOptionPane.WARNING_MESSAGE);
							}
						}
					}
				} catch (Exception e) {
					e.printStackTrace();
				}
			}
		});
		btnCheck.addActionListener(new ActionListener() {
			public void actionPerformed(ActionEvent arg0) {
			}
		});
		panel_1.add(btnCheck);
	}
	
	private void loadModel(File modelFile) {
		Reader reader = new Reader();
		Writer writer = new Writer();
		try {
			project = reader.readAlloy(null, modelFile.getAbsolutePath());
			LOG.debug(project.getModel().toString());
			refreshTree();
		} catch (Exception e1) {
			// TODO Auto-generated catch block
			e1.printStackTrace();
		}
	}
	
	private void saveInstance(File instanceFile) {
		Writer writer = new Writer();
		try {
			writer.writeAlloy(project.getInstance(), project.getModel(), instanceFile);
		} catch (Exception e1) {
			// TODO Auto-generated catch block
			e1.printStackTrace();
		}
	}
	
	private void refreshTree() {
		tree.setExpandsSelectedPaths(true);
		DefaultMutableTreeNode root = new DefaultMutableTreeNode("ROOT");
		DefaultTreeModel treeModel = new DefaultTreeModel(root, true);
		for(ModelObject mo : project.getModel().getObjects()){
			DefaultMutableTreeNode child = new DefaultMutableTreeNode(mo);
			treeModel.insertNodeInto(child, root, root.getChildCount());
			for (ModelRelation mr : mo.getAllRelations()) {
				treeModel.insertNodeInto(new DefaultMutableTreeNode(mr,false), child, child.getChildCount());
			}
			/*if (project.getInstance() != null && project.getInstance().getInheritanceMap().get(mo) != null) {
				for(InstanceObject io : project.getInstance().getInheritanceMap().get(mo)) {
					treeModel.insertNodeInto(new DefaultMutableTreeNode(io,false), child, child.getChildCount());
				}
				//treeModel.insertNodeInto(new DefaultMutableTreeNode("<<add "+mo.getName()+">>"), child, child.getChildCount());
			}*/
		}	
		tree.setModel(treeModel);
		// expand all
		for (int i = 0; i < tree.getRowCount(); i++) {
		    tree.expandRow(i);
		}
		// disable collapsing
		tree.setToggleClickCount(0);
		// hide ROOT
		tree.setRootVisible(false);
	}
	
	private void refreshGraph() {
		String s = GraphUtil.dotGraph(project.getInstance());
		LOG.debug(s);
		InputStream is = new ByteArrayInputStream(s.getBytes());
		
		Parser program = new Parser(is,System.err);
		try {
		    //program.debug_parse(4);
		    program.parse();
		} catch(Exception ex) {
		    System.err.println("Exception: " + ex.getMessage());
		    ex.printStackTrace(System.err);
		    System.exit(1);
		}
		Graph graph = null;
		graph = program.getGraph();
		Object connector = null;
		try {
			connector = Runtime.getRuntime().exec("C:\\Users\\N42\\workspace\\mgr\\graphviz-2.36\\release\\bin\\dot.exe");
		    } catch(Exception ex) {
			System.err.println("Exception while setting up Process: " + ex.getMessage() + "\nTrying URLConnection...");
			connector = null;
		    }
		if(connector != null) {
			if(!GrappaSupport.filterGraph(graph,connector)) {
			    System.err.println("ERROR: somewhere in filterGraph");
			}
			if(connector instanceof Process) {
			    try {
				int code = ((Process)connector).waitFor();
				if(code != 0) {
				    System.err.println("WARNING: proc exit code is: " + code);
				}
			    } catch(InterruptedException ex) {
				System.err.println("Exception while closing down proc: " + ex.getMessage());
				ex.printStackTrace(System.err);
			    }
			}
			connector = null;
		    }
		graph.repaint();
	}

}
